(declare-sort S0 0)

(declare-const i3 Int)
(declare-const i4 Int)
(declare-const i12 Int)
(declare-const arr-1372044138120344436_-210295852911674790-0 (Array Bool Int))
(declare-const arr-1372044138120344436_-8378710954361435089-0 (Array Bool S0))
(declare-const v9 Bool)
(declare-const arr-1372044138120344436_-8453188389653899215-0 (Array Bool (Array S0 Int)))
(declare-const arr--210295852911674790_-2811811931679789589-0 (Array Int (Array Bool (Array S0 Int))))
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const v16 Bool)
(declare-const arr--2811811931679789589_1372044138120344436-0 (Array (Array Bool (Array S0 Int)) Bool))
(assert (or v9 (= 698 47) (= 698 47)))
(assert (or (select arr--2811811931679789589_1372044138120344436-0 (select arr--210295852911674790_-2811811931679789589-0 698)) (>= (abs i4) (mod i12 i12)) v16))
(assert (or (= 698 47) (select arr--2811811931679789589_1372044138120344436-0 arr-1372044138120344436_-8453188389653899215-0) v14))
(assert (or v15 v16 v15))
(check-sat)
